{-# LANGUAGE TemplateHaskell, TypeFamilies, QuasiQuotes, StandaloneDeriving,
  FlexibleInstances, FlexibleContexts, UndecidableInstances, GADTs,
  MultiParamTypeClasses, TypeOperators, EmptyDataDecls  #-}

{- |

Module      :  Data.Yoko.Generic
Copyright   :  (c) The University of Kansas 2011
License     :  BSD3

Maintainer  :  nicolas.frisby@gmail.com
Stability   :  experimental
Portability :  see LANGUAGE pragmas (... GHC)

Representations of many Haskell types as compositions of "Data.Yoko.Core"
types.

-}

module Data.Yoko.Generic
  (module Data.Yoko.Generic, module Data.Yoko.CoreTypes) where

import Data.Yoko.CoreTypes
import qualified Data.Yoko.Core as Core

import Type.Yoko.Type
import Type.Yoko.TSTSS
--import Type.Yoko.Universe ((:::)(..))

import qualified Control.Arrow as Arrow
                       

{- | @RM@ stands is for \"recursively mediated\", and @m@ is the \"mediator (of
recursive occurrences)\".

@
  data instance RM m V
  data instance RM m U = U
  newtype instance RM m (D a) = D a
  newtype instance RM m (R t) = R (Med m t)
  newtype instance RM m (F f c) = F (f (RM m c))
  newtype instance RM m (FF ff c d) = FF (ff (RM m c) (RM m d))
  newtype instance RM m (M i c) = M (RM m c)
@

-}
data family RM m c
data instance RM m V
data instance RM m U = U
newtype instance RM m (D a) = D a
newtype instance RM m (R t) = R (Med m t)
newtype instance RM m (F f c) = F (f (RM m c))
newtype instance RM m (FF ff c d) =
  FF (ff (RM m c) (RM m d))
newtype instance RM m (M i c) = M (RM m c)

infixr 6 :*
data instance RM m (c :* d) = RM m c :* RM m d

-- | In @yoko@, the 'N' core type is used for a lightweight representation of
-- constructor types -- each will define its own instance of @RM (N _)@.
type RMN m dc = RM m (N dc)

type RMI = RM IdM
type RMNI dc = RMN IdM dc


class Core2RMI c where core2RMI :: c -> RMI c
instance Core2RMI U where core2RMI _ = U
instance Core2RMI (D a) where core2RMI (Core.D a) = D a
instance Core2RMI (R t) where core2RMI (Core.R a) = R a
instance (Functor f, Core2RMI c) => Core2RMI (F f c) where
  core2RMI (Core.F x) = F $ fmap core2RMI x
instance (FunctorTSTSS ff, Core2RMI c, Core2RMI d) => Core2RMI (FF ff c d) where
  core2RMI (Core.FF x) = FF $ fmapTSTSS core2RMI core2RMI x
instance Core2RMI c => Core2RMI (M i c) where core2RMI (Core.M x) = M $ core2RMI x
instance (Core2RMI c, Core2RMI d) => Core2RMI (c :* d) where
  core2RMI (x Core.:* y) = core2RMI x :* core2RMI y


-- | @Generic@ represents a recursion-mediated type @N a@ as a
-- recursion-mediated @Rep a@. The opposite of \"representation\" is (the
-- represented) \"object\".
class Core2RMI (Rep a) => Generic a where
  rep :: RM m (N a) -> RM m (Rep a)
  obj :: RM m (Rep a) -> RM m (N a)

{-asRep :: (Generic a, Generic b) => (RM m (Rep a) -> RM m (Rep b)) -> RM m (N a) -> RM m (N b)
asRep f = obj . f . rep

asGist :: (Gist c, Gist d) => (Gst c m -> Gst d n) -> RM m c -> RM n d
asGist f = frip . f . gist

convertR :: (Gist c, Gst c m ~ Gst c n) => RM m c -> RM n c
convertR = asGist id-}


-- | It's a regular pattern throughout @yoko@ for a type constructor to take a
-- mediator as its penultimate parameter. Also, mediators tend to occur as
-- arguments to type families, so it is helpful to ascribe them.
atM2 :: t m a -> [qP|m|] -> t m a
atM2 x _ = x

atM1 :: t m -> [qP|m|] -> t m
atM1 x _ = x

-- @gist@ folds the mediator @m@ into the type and forgets all the frippery of
-- the core representation. (The opposite of \"gist\" is \"frippery\".)
class Gist c where
  gist :: RM m c -> Gst c m
  frip :: Gst c m -> RM m c

{-
data AsRep u t where AsRep :: u (Rep t) -> AsRep u t
obvious_inhabitation ''AsRep

data GistD c where GistD :: Gist c => GistD c
obvious_inhabitation ''GistD
gistD :: GistD c -> RM m c -> Gst c m; gistD GistD = gist
fripD :: GistD c -> Gst c m -> RM m c; fripD GistD = frip
-}


type family Gst c m
type instance Gst (F f c) m = f (Gst c m)
type instance Gst (FF Either c d) m = Either (Gst c m) (Gst d m)
type instance Gst (FF (,) c d) m = (,) (Gst c m) (Gst d m)
type instance Gst (D a) m = a
type instance Gst (M i c) m = Gst c m
type instance Gst (R t) m = Med m t
type instance Gst U m = ()
type instance Gst V m = Core.V
type instance Gst (N n) m = Gst (Rep n) m

instance (Functor f, Gist c) => Gist (F f c) where
  gist (F x) = fmap gist x; frip = F . fmap frip
instance (Gist c, Gist d) => Gist (FF Either c d) where
  gist = (gist Arrow.+++ gist) . unFF
  frip = FF . (frip Arrow.+++ frip)
instance (Gist c, Gist d) => Gist (FF (,) c d) where
  gist = (gist Arrow.*** gist) . unFF
  frip = FF . (frip Arrow.*** frip)
instance Gist (D a) where gist (D x) = x; frip = D
instance Gist c => Gist (M i c) where
  gist = gist . unM; frip = M . frip
instance Gist (R t) where gist (R x) = x; frip = R
instance Gist U where gist _ = (); frip _ = U
instance Gist V where gist = absurd "gist[V]"; frip _ = void "gist[V]"
instance (Generic t, Gist (Rep t)) => Gist (N t) where
  gist = gist . rep; frip = obj . frip



unD :: RM m (D a) -> a
unD (D x) = x

unM :: RM m (M i c) -> RM m c
unM (M x) = x

unR :: RM m (R t) -> Med m t
unR (R x) = x
deriving instance Eq (Med m t) => Eq (RM m (R t))
deriving instance Show (Med m t) => Show (RM m (R t))

instance Eq (RM m V) where _ == _ = True -- undefined?
instance Show (RM m V) where show _ = "<void>"
void :: String -> RM m V
void n = error $ "GenericR.void: " ++ n
absurd :: String -> RM m V -> a
absurd n = error $ "GenericR.absurd: " ++ n

unF (F x) = x
unFF (FF x) = x
deriving instance Eq (ff (RM m c) (RM m d)) => Eq (RM m (FF ff c d))
deriving instance Show (ff (RM m c) (RM m d)) => Show (RM m (FF ff c d))

unAF (x :* y) = (x, y)
deriving instance (Eq (RM m c), Eq (RM m d)) => Eq (RM m (AF c d))
deriving instance (Show (RM m c), Show (RM m d)) => Show (RM m (AF c d))


deriving instance Eq t => Eq (RM m (D t))
deriving instance Eq (f (RM m c)) => Eq (RM m (F f c))
deriving instance Eq (RM m U)
deriving instance Eq (RM m c) => Eq (RM m (M i c))

repEq :: (Generic t, Eq (RM m (Rep t))) => RMN m t -> RMN m t -> Bool
repEq x y = rep x == rep y




concat `fmap` mapM derive [''RM]
